\begin{tabbing}
$\forall$\=$k$:Knd, $T$,$B$:Type, $l$:IdLnk, ${\it ds}$:fpf(Id; $x$.Type), ${\it tg}$:Id, $f$:(decl{-}state(${\it ds}$)$\rightarrow$$T$$\rightarrow$$B$),\+
\\[0ex]${\it es}$:event\_system\{i:l\}. usends1{-}p(${\it es}$;${\it ds}$;$k$;$T$;$l$;${\it tg}$;$B$;$f$) $\in$ prop\{i:l\}
\-
\end{tabbing}